package interfaces;

import java.util.Date;

import tdg.contract.semanticAnnotations.ImportClass;
import tdg.contract.semanticAnnotations.Init;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Query;



@Init ({"getFechaDeCompra()!=null"})
@Inv ({""})

public interface ILineaDeProducto {
	
	@Query
	public Date getFechaDeCompra();
	
	@Query
	public int getCodigo();
	
	@Pre ({"nuevaFecha!=null #NullPointerException"})
	@Pos ({"getFechaCompra()==nuevaFecha && getCodigo()==getCodigo()@pre"})
	public void setFechaDeCompra(Date nuevaFecha);
	
	@Pre ({"c>=0 && c<=Integer.MAX_VALUE #IllegalArgumentException"})
	@Pos({"getFechaCompra()==gerFechaCompra()@pre && getCodigo()==c"})
	public void setCodigo(int c);
}
